Step of Proof: outr_wf 12,41

Inference at * 1 1 
Iof proof for Lemma outr wf:



1. A : Type
2. B : Type
3. x1 : A
4. False
  outr(inl x1 )  B 
latex

 by (Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term) 
latex


 .


DefinitionsFalse

origin